structure Systeml :> Systeml = struct

(* This is the UNIX implementation of the Systeml functionality.  It is the
   very first thing compiled by the HOL build process so it absolutely
   can not depend on any other HOL source code. *)

structure Path =  OS.Path
structure Process = OS.Process
structure FileSys = OS.FileSys

local
  open Process
  fun concat_wspaces munge strl = String.concatWith " " (map munge strl)
in

  val unix_meta_chars = [#"'", #"\"", #"|", #" ", #">", #"\t", #"\n", #"<",
                         #"\\", #"#"]
  fun is_meta c = List.exists (fn y => c = y) unix_meta_chars
  fun is_meta_string(s,i) = if i >= size s then false
                            else if is_meta (String.sub(s,i)) then true
                            else is_meta_string(s, i + 1)
  fun unix_trans c = if is_meta c then "\\" ^ str c else str c

  fun protect s = if is_meta_string(s,0) then String.translate unix_trans s
                  else s

  val systeml = system o concat_wspaces protect
  fun systeml_out {outfile} c =
    system (concat_wspaces protect c ^ " > " ^ protect outfile ^ " 2>&1")

  fun get_first f [] = NONE
    | get_first f (h::t) = case f h of NONE => get_first f t
                                     | x => x


  fun find_my_path () = let
    (* assumes directory hasn't been changed yet *)
    val myname = CommandLine.name()
    val {dir,file} = Path.splitDirFile myname
  in
    if dir = "" then let
        val pathdirs = String.tokens (fn c => c = #":")
                                     (valOf (Process.getEnv "PATH"))
        open FileSys
        fun checkdir d = let
          val f = Path.concat(d,file)
        in
          if access(f, [A_READ, A_EXEC]) then SOME f else NONE
        end
      in
        valOf (get_first checkdir pathdirs)
      end
    else
      Path.mkAbsolute {path = myname, relativeTo = FileSys.getDir()}
  end

  val system_ps = Process.system
  (* see winNT-systeml.sml for an explanation of why what is a synonym under
     unix needs to be slightly different on Windows. *)

  fun xable_string s = s

  fun mk_xable file =
    let
      val r = systeml ["chmod", "a+x", file]
    in
      if Process.isSuccess r then r
      else if FileSys.access (file,[FileSys.A_EXEC]) then
          (* if we can execute it, then continue with a warning *)
          (* NB: MoSML docs say FileSys.access uses real uid/gid, not effective uid/gid,
             so this test may be bogus if we are setuid.  This is unlikely(!). *)
          (print ("Non-fatal warning: couldn't set world execute permission on "^file^",\n  but continuing anyway since at least the current user has execute permission.\n");
           OS.Process.success)
      else (print ("unable to set execute permission on "^file^".\n");
            OS.Process.failure)
    end


fun normPath s = Path.toString(Path.fromString s)

fun fullPath slist =
    normPath (List.foldl (fn (p1,p2) => Path.concat(p2,p1))
                         (hd slist) (tl slist))


(* these values are filled in by configure.sml *)
val HOLDIR = ""
val MOSMLDIR = ""
val POLYMLLIBDIR = ""
val POLY = ""
val POLYC = ""
val POLY_VERSION = PolyML.Compiler.compilerVersionNumber
val POLY_LDFLAGS = []
val POLY_LDFLAGS_STATIC = []
val CC = ""
val OS = ""

val DEPDIR = ""
val GNUMAKE = ""
val DYNLIB = ""
val version = ""
val ML_SYSNAME = ""
val release = ""
val DOT_PATH = ""
val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"]

val isUnix = true

val pointer_eq = PolyML.pointerEq

fun exec (x as (comm,args)) =
    (* macos execv fails if the calling process is multi-threaded. *)
    (* Can't lift the check out of the function body because of the value
       restriction *)
    if OS <> "macosx" then Posix.Process.exec x
    else OS.Process.exit (systeml (comm::tl args))


val build_log_dir = fullPath [HOLDIR, "tools-poly", "build-logs"]
val build_log_file = fullPath [build_log_dir, "current-build-log"]
val make_log_file = "current-make-log";
val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY"

fun base_interactive state scripts =
    [POLY, "-q", "--use", fullPath [HOLDIR, "bin", "hol.ML"], state] @ scripts


fun emit_hol_script target exe script =
  let
    val ostrm = TextIO.openOut target
    fun output s = TextIO.output(ostrm, s)
  in
    output "#!/bin/sh\n";
    output "# The bare HOL script\n";
    output "# (automatically generated by HOL configuration)\n\n";
    output (fullPath [HOLDIR, "bin", "buildheap"] ^
            " --gcthreads=1 --repl --holstate=" ^ exe ^ " " ^
            String.concatWith " " script ^ " \"$@\"\n");
    TextIO.closeOut ostrm;
    mk_xable target
  end;

  fun emit_hol_unquote_script target exe s =
      let val ostrm = TextIO.openOut target
          fun output s = TextIO.output(ostrm, s)
          val qfilter = protect (fullPath [HOLDIR, "bin", "unquote"])
          val script =
            List.map (fn s => protect (fullPath [HOLDIR, "tools-poly", s]))
                     s
      in
        output "#!/bin/sh\n";
        output "# The HOL script (with quote preprocessing)\n";
        output "# (automatically generated by HOL configuration)\n\n";
        output (String.concatWith " "
                   ([qfilter, "|"] @ base_interactive exe script) ^ "\n");
        TextIO.closeOut ostrm;
        mk_xable target
      end;
end (* local *)

fun bindstr mlcode =
    "val _ = CompilerSpecific.quietbind \"" ^ String.toString mlcode ^ "\""

end; (* struct *)
